Issue3457.agda:4,25-35
Not in scope:
  Fresh-name at Issue3457.agda:4,25-35
when scope checking Fresh-name
